Notes (Week 2 Tuesday)

Problem 1: Prove that the definition inference rule for Odd also
applies to Odd', that is, the judgement Odd' also holds of the
successor of any even number.

We want to prove

n Even
---------
(S n) Odd'


We proceed by rule induction on Even, since we want to show
something is true of all Even numbers.


There are two inference rules for Even, so rule induction
requires two steps.

(P 0), !n. (P n |- P (S (S n))) |- !n. (Even n |- P n)

(-- yuck, this syntax doesn't nest well. --)


OK, we perform rule induction on the shape of Even, with
P(n) = (S n) Odd'.

The base case corresponds to E1: show P 0.

P 0 == (S 0) Odd'

This is easy, here is a derivation:

---------- by O1
(S 0) Odd'


The inductive case corresponds to E2:
assume P n and show P (S (S n)).

P n == (S n) Odd'
and
P (S (S n)) == (S (S (S n))) Odd'

Show:

(S n) Odd' |- (S (S (S n))) Odd'

Proof:


------------------------ as a local axiom
(S n) Odd' |- (S n) Odd'
-------------------------------- O2
(S n) Odd' |- (S (S (S n))) Odd'


QED.

Problem 2: Prove our two definitions of the matched-parens
language are equivalent.


The first step is to prove that all elements of L and N are in M.
This is not a conceptually complicated proof, as the inference
rules for L and N are specialisations of the inference rules of
M. However, they are defined in terms of each other, so we must
prove by simultaneous induction that:

s L       s N
---  and  ---
s M       s M


This is an instance of simultaneous induction proving P(s) and
Q(s) where P(s) is just s M and Q(s) is also just s M.

The induction is rule induction on the rule definition of L/N.

There are 3 goals.

The base case comes from rule L_E, which shows ε L. We must show
P(ε) == ε M.

This is just rule M_E:

---- M_E
ε  M

The first inductive case comes from rule N_N, s L |- (s) N.

We may assume the inductive hypothesis about s, P(s) == s M, and
must show the goal Q( (s) ) == (s) M. Remember that we are
proving P(s) about things in L and Q(s) about things in N
(although P and Q are the same here).

Again, the proof is easy, using rule M_N:

----------  axiom
s M |- s M
------------ M_N
s M |- (s) M


The second inductive case is associated with the rule L_J,
    s1 N, s2 L |- s1 s2 L.

There are two inductive hypotheses, Q(s1) == s1 M and P(s2) == s2 M.
The goal is P ( s1 s2 ) == s1 s2 M.

Once again, the proof is easy, and just uses rule M_J. I will
skip typing it out.




Problem 2b: How do we prove that M is in L?


The point of splitting M into L/N was to disambiguate its
grammar. The rules for M permit juxtaposition/concatenation in
any structure. The rules for L/N enforce each juxtaposition in L
to be built in a right-associated way.

I ran out of time to solve this in the lecture. We could get
started by using rule induction on the structure of M. The M_E ε
case and the M_N (s) case are easy. The complication is the
justaposition rule M_J:

s1 M     s2 M
-------------
   s1 s2 M

This rule can be used when s1 is in M and L but not in N, i.e.
when s1 is a concatenation of elements of N. We know s1 was
proven to be in M, but we might need to go arbitrarily deep into
that proof before we find something in N.

In conclusion, I think we need to prove this concatenation rule
as a lemma about the L judgement:

s1 L     s2 L
-------------
   s1 s2 L

This seems reasonable. Recall the L judgement holds of lists of
things where the N judgement holds at each element. It seems
reasonable that we can append two lists and reassociate it into a
single list. However, doing the reassociaton might take an
arbitrary number of steps,
e.g. if s1 ≈ [a, b, c] ≡ a : (b : (c : [])) and s2 ≈ [x, y] ≡ x : (y : []),
doing the concatenation to get ≈ a : (b : (c : (x : (y : [])))) takes 3 steps.


So, use induction! Let's prove the concatenation property about
L. However, it has two parameters s1 and s2. We want to induct
over one of them and leave the other fixed. This is getting a bit
complicated, so let's pick it up again at the start of Thursday's
lecture.